\begin{tabbing}
$\forall$${\it es}$:ES, $b$:$\mathbb{B}$, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$\mathbb{B}$)\} .
\\[0ex](($x$ when $e$) = $b$)
\\[0ex]$\Rightarrow$ (($x$ initially@loc($e$)  = ($\neg_{b}$$b$) $\in$ $\mathbb{B}$) $\vee$ ($\exists$${\it e'}$:E. (${\it e'}$ $\leq$loc $e$  \& ($x$ when ${\it e'}$) = ($\neg_{b}$$b$) $\in$ $\mathbb{B}$)))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex]((${\it e'}$ $<$loc $e$)
\\[0ex]\& ($x$ when ${\it e'}$) = ($\neg_{b}$$b$) $\in$ $\mathbb{B}$
\\[0ex]\& ($x$ after ${\it e'}$) = $b$
\\[0ex]\& $\forall$${\it e''}$$\in$(${\it e'}$,$e$].($x$ when ${\it e''}$) = $b$
\\[0ex]\& $\forall$${\it e''}$$\in$[${\it e'}$,$e$).($x$ after ${\it e''}$) = $b$))
\-
\end{tabbing}